Termination w.r.t. Q proof of /tmp/tmpxsjYOH/linear2.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a, f(a, f(a, f(x, b)))) → f(f(a, f(a, f(a, x))), b)
f(f(f(a, x), b), b) → f(f(a, f(f(x, b), b)), b)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

f(a, f(a, f(a, f(x, b)))) → f(f(a, f(a, f(a, x))), b)
f(f(f(a, x), b), b) → f(f(a, f(f(x, b), b)), b)

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

F(f(f(a, x), b), b) → F(f(x, b), b)
F(f(f(a, x), b), b) → F(f(a, f(f(x, b), b)), b)
F(f(f(a, x), b), b) → F(a, f(f(x, b), b))
F(a, f(a, f(a, f(x, b)))) → F(a, f(a, f(a, x)))
F(a, f(a, f(a, f(x, b)))) → F(a, f(a, x))
F(a, f(a, f(a, f(x, b)))) → F(a, x)
F(a, f(a, f(a, f(x, b)))) → F(f(a, f(a, f(a, x))), b)
F(f(f(a, x), b), b) → F(x, b)

The TRS R consists of the following rules:

f(a, f(a, f(a, f(x, b)))) → f(f(a, f(a, f(a, x))), b)
f(f(f(a, x), b), b) → f(f(a, f(f(x, b), b)), b)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

F(f(f(a, x), b), b) → F(f(x, b), b)
F(f(f(a, x), b), b) → F(f(a, f(f(x, b), b)), b)
F(f(f(a, x), b), b) → F(a, f(f(x, b), b))
F(a, f(a, f(a, f(x, b)))) → F(a, f(a, f(a, x)))
F(a, f(a, f(a, f(x, b)))) → F(a, f(a, x))
F(a, f(a, f(a, f(x, b)))) → F(a, x)
F(a, f(a, f(a, f(x, b)))) → F(f(a, f(a, f(a, x))), b)
F(f(f(a, x), b), b) → F(x, b)

The TRS R consists of the following rules:

f(a, f(a, f(a, f(x, b)))) → f(f(a, f(a, f(a, x))), b)
f(f(f(a, x), b), b) → f(f(a, f(f(x, b), b)), b)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ RuleRemovalProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F(f(f(a, x), b), b) → F(f(x, b), b)
F(f(f(a, x), b), b) → F(f(a, f(f(x, b), b)), b)
F(f(f(a, x), b), b) → F(x, b)

The TRS R consists of the following rules:

f(a, f(a, f(a, f(x, b)))) → f(f(a, f(a, f(a, x))), b)
f(f(f(a, x), b), b) → f(f(a, f(f(x, b), b)), b)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

F(f(f(a, x), b), b) → F(f(x, b), b)
F(f(f(a, x), b), b) → F(x, b)

Used ordering: POLO with Polynomial interpretation [25]:

POL(F(x₁, x₂)) = x₁ + x₂
POL(a) = 2
POL(b) = 0
POL(f(x₁, x₂)) = x₁ + x₂

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ RuleRemovalProof

              ↳ QDP

                ↳ QDPOrderProof

          ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F(f(f(a, x), b), b) → F(f(a, f(f(x, b), b)), b)

The TRS R consists of the following rules:

f(a, f(a, f(a, f(x, b)))) → f(f(a, f(a, f(a, x))), b)
f(f(f(a, x), b), b) → f(f(a, f(f(x, b), b)), b)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

F(f(f(a, x), b), b) → F(f(a, f(f(x, b), b)), b)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Matrix interpretation [3]:
Non-tuple symbols:

M( a ) =

/	0	\
\	0	/

M( f(x₁, x₂) ) =

/	1	\
\	0	/

/	0	0	\
\	0	0	/

x₁

/	0	1	\
\	1	0	/

x₂

M( b ) =

/	0	\
\	1	/

Tuple symbols:

M( F(x₁, x₂) ) =

[

]

x₁

[

]

x₂

Matrix type:
We used a basic matrix type which is not further parametrizeable.

As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
The following usable rules [17] were oriented:

f(a, f(a, f(a, f(x, b)))) → f(f(a, f(a, f(a, x))), b)
f(f(f(a, x), b), b) → f(f(a, f(f(x, b), b)), b)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ RuleRemovalProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

          ↳ QDP

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f(a, f(a, f(a, f(x, b)))) → f(f(a, f(a, f(a, x))), b)
f(f(f(a, x), b), b) → f(f(a, f(f(x, b), b)), b)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ RuleRemovalProof

Q DP problem:
The TRS P consists of the following rules:

F(a, f(a, f(a, f(x, b)))) → F(a, f(a, f(a, x)))
F(a, f(a, f(a, f(x, b)))) → F(a, f(a, x))
F(a, f(a, f(a, f(x, b)))) → F(a, x)

The TRS R consists of the following rules:

f(a, f(a, f(a, f(x, b)))) → f(f(a, f(a, f(a, x))), b)
f(f(f(a, x), b), b) → f(f(a, f(f(x, b), b)), b)

F(a, f(a, f(a, f(x, b)))) → F(a, f(a, x))
F(a, f(a, f(a, f(x, b)))) → F(a, x)

Used ordering: POLO with Polynomial interpretation [25]:

POL(F(x₁, x₂)) = x₁ + x₂
POL(a) = 2
POL(b) = 0
POL(f(x₁, x₂)) = x₁ + x₂

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ RuleRemovalProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

F(a, f(a, f(a, f(x, b)))) → F(a, f(a, f(a, x)))

The TRS R consists of the following rules:

f(a, f(a, f(a, f(x, b)))) → f(f(a, f(a, f(a, x))), b)
f(f(f(a, x), b), b) → f(f(a, f(f(x, b), b)), b)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.